Nuprl Definition : detach
13,42
postcript
pdf
T
-Detach(
A
) ==
x
:
T
. Dec(
A
(
x
))
latex
Up
gen
algebra
1
Wellformedness Lemmas
detach
wf
Definitions
x
:
A
.
B
(
x
)
,
Dec(
P
)
origin
x:T. Dec(A(x)) x:T. Dec(A(x)) x:A. B(x)